\begin{tabbing}
$\forall$$E$:Type, ${\it pred?}$:($E$$\rightarrow$(?$E$)).
\\[0ex]SWellFounded(($\neg$($\uparrow$first($y$))) c$\wedge$ ($x$ = pred($y$) $\in$ $E$))
\\[0ex]$\Rightarrow$ \=($\forall$$e$,${\it e'}$:$E$.\+
\\[0ex](${\it e'}$ $\in$ eventlist(${\it pred?}$; $e$))
\\[0ex]$\Leftarrow\!\Rightarrow$ (${\it e'}$ rel\_star($E$; ($\lambda$$x$,$y$. ($\neg$($\uparrow$first($y$))) c$\wedge$ ($x$ = pred($y$) $\in$ $E$))) $e$))
\-
\end{tabbing}